le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
↳ QTRS
↳ Overlay + Local Confluence
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
LE(s(x), s(y)) → LE(x, y)
EQ(s(x), s(y)) → EQ(x, y)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
IF2(false, x, y, xs) → DEL(x, xs)
MINSORT(cons(x, y)) → MIN(x, y)
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
MINSORT(cons(x, y)) → DEL(min(x, y), cons(x, y))
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
MIN(x, cons(y, z)) → LE(x, y)
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
DEL(x, cons(y, z)) → EQ(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LE(s(x), s(y)) → LE(x, y)
EQ(s(x), s(y)) → EQ(x, y)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
IF2(false, x, y, xs) → DEL(x, xs)
MINSORT(cons(x, y)) → MIN(x, y)
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
MINSORT(cons(x, y)) → DEL(min(x, y), cons(x, y))
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
MIN(x, cons(y, z)) → LE(x, y)
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
DEL(x, cons(y, z)) → EQ(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
IF2(false, x, y, xs) → DEL(x, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
IF2(false, x, y, xs) → DEL(x, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
IF2(false, x, y, xs) → DEL(x, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
min(x, nil) → x
if1(true, x, y, xs) → min(x, xs)
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
if1(false, x, y, xs) → min(y, xs)
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
minsort(nil)
minsort(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
min(x, nil) → x
if1(true, x, y, xs) → min(x, xs)
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
if1(false, x, y, xs) → min(y, xs)
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
POL(0) = 0
POL(MINSORT(x1)) = x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = x2
POL(false) = 0
POL(if1(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(if2(x1, x2, x3, x4)) = 1 + x3 + x4
POL(le(x1, x2)) = 1
POL(min(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ PisEmptyProof
↳ QTRS
min(x, nil) → x
if1(true, x, y, xs) → min(x, xs)
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
if1(false, x, y, xs) → min(y, xs)
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
DEL'(x49, cons(y40, z7)) → EQ(x49, y40)
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
MIN(x23, cons(y18, z2)) → LE(x23, y18)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
DEL(x49, cons(y40, z7)) → EQ(x49, y40)
EQ(s(x99), s(y82)) → EQ(x99, y82)
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
LE(s(x176), s(y146)) → LE(x176, y146)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
DEL'(x49, cons(y40, z7)) → EQ(x49, y40)
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
MIN(x23, cons(y18, z2)) → LE(x23, y18)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
DEL(x49, cons(y40, z7)) → EQ(x49, y40)
EQ(s(x99), s(y82)) → EQ(x99, y82)
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
LE(s(x176), s(y146)) → LE(x176, y146)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x176), s(y146)) → LE(x176, y146)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x176), s(y146)) → LE(x176, y146)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x176), s(y146)) → LE(x176, y146)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x99), s(y82)) → EQ(x99, y82)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x99), s(y82)) → EQ(x99, y82)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x99), s(y82)) → EQ(x99, y82)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x', nil) → x'
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs: